Inference at * 1 
Iof proof for Lemma can-apply-p-co-filter:



1. T : Type
2. P : T
3. f : x:T. Dec(P(x))
4. x : T
  (isl(case f(x) of inl(p) => inr p  | inr(p) => inl x ))  (P(x)) 

latex

 by ((((GenConcl f(x) = z) 
CollapseTHENA (Auto))) 
CollapseTHEN (((D (-2)) 
CollapseTHEN (((
CoReduce 0) 
CollapseTHEN (Auto)))))) 

latex

Co.

Definitions	s = t, Dec(P), x(s), f(a), , x:AB(x), P  Q, left + right, False, b, P  Q, P & Q, P  Q, P  Q, True, t  T, A, x:A. B(x)
Lemmas	decidable wf, false wf, true wf, not wf